ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), k:Knd, l:IdLnk, tg:Id, n:,
f:(decl-state(ds)ma-valtype(da; k)fpf-cap(da; Kind-deq; rcv(l,tg); void)).
msg-spec1(k; l; tg; n; s,v.f(s,v))  msg-spec(ds; da) 

latex

Definitions	void, Type, t  T, x:A. B(x), rcv(l,tg), Kind-deq, Knd, x.A(x), x. t(x), fpf-cap(f; eq; x; z), type List, ma-valtype(da; k), x:AB(x), decl-state(ds), , x:A  B(x), [], f(a), x(s1,s2), cons(car; cdr), <a, b>, msg-item(ds; da; k; l), P  Q, False, A, A  B, , {x:A| B(x)} , IdLnk, t.2, t.1, msg-spec1(k; l; tg; n; s,v.f(s;v)), msg-spec(ds; da), Id, fpf(A; a.B(a))
Lemmas	fpf wf, Id wf, fpf-single wf, pi1 wf, pi2 wf, IdLnk wf, msg-item wf, nat wf, decl-state wf, ma-valtype wf, fpf-cap wf, Knd wf, Kind-deq wf, rcv wf